(set-logic QF_BV)
(declare-fun x () (_ BitVec 10))
(declare-fun y () (_ BitVec 10))
(declare-fun z () (_ BitVec 9))
(declare-fun b () Bool)
(assert 
  (let ((e9 (ite b ((_ sign_extend 1) z) y))) 
  (let ((e10 (bvand z z))) 
  (let ((e15 (bvadd y x))) 
  (let ((e19 (bvadd ((_ sign_extend 1) e10) e9))) 
  (let ((e27 (ite (bvsge (_ bv0 10) x) (_ bv1 1) (_ bv0 1)))) 
  (let ((e32 (= ((_ zero_extend 9) e27) e19))) 
  (let ((e41 (bvult (_ bv0 9) z))) 
  (let ((e49 (bvsge e15 y))) 
  (let ((e53 (bvsge y (_ bv0 10)))) 
  (let ((e62 (bvult (_ bv0 10) x))) 
  (let ((e78 e41)) 
  (let ((e84 (xor e53 true))) 
  (let ((e102 e32)) 
  (let ((e104 e84)) 
  (let ((e106 e49)) 
  (let ((e108 (xor e78 e104))) 
  (let ((e109 e102)) 
  (let ((e112 (not e108))) 
  (let ((e115 e109)) 
  (let ((e116 (not e62))) 
  (let ((e118 e116)) 
  (let ((e119 (xor e106 false))) 
  (let ((e120 (and e118 e115))) 
  (let ((e121 e119)) 
  (let ((e122 (=> e121 e120))) 
  (let ((e123 (not e122))) 
  (let ((e124 (xor e112 e123))) 
  (let ((e125 e124)) 
  (let ((e126 e125)) 
  (let ((e127 e126)) e127)))))))))))))))))))))))))))))))
(check-sat)

